$e$ = ${\it e'}$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$eqof(1of(2of(${\it es}$)))($e$,${\it e'}$)